Skip to content

Adds additional properties to {Left,Right}Module #2906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
jamesmckinna merged 9 commits into from
Jan 14, 2026
Merged

Adds additional properties to {Left,Right}Module #2906

jamesmckinna merged 9 commits into from
Jan 14, 2026

Conversation

@bsaul
Copy link
Contributor

@bsaul bsaul commented Jan 5, 2026

This PR adds additional properties to Algebra.Module.Properties.LeftModule.

NOTE: I can also add the corresponding properties to RightModule, but I'll wait for any discussions of naming and appropriateness of the LeftModule properties to conclude first.

jamesmckinna
jamesmckinna requested changes Jan 8, 2026
View reviewed changes
Copy link
Collaborator

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very nice addition, but I think the suggested renaming/refactorings make it 'better'?
(Open to debate on this, though! esp. with any 2nd reviewer...)

@bsaul @jamesmckinna
Update src/Algebra/Module/Properties/LeftModule.agda
c3b8f63 
using suggestion

Co-authored-by: jamesmckinna <[email protected]>
jamesmckinna
jamesmckinna approved these changes Jan 9, 2026
View reviewed changes
Copy link
Collaborator

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great now! Thanks for the prompt response to my feedback.

@jamesmckinna jamesmckinna added this to the v2.4 milestone Jan 9, 2026
@Taneb
Copy link
Member

Taneb commented Jan 9, 2026

This is very good! But I'd like to see the corresponding proofs on right modules as well in this PR

@jamesmckinna
Copy link
Collaborator

jamesmckinna commented Jan 9, 2026

I agree with @Taneb regarding the RightModule case, but I'd understood that was part of the original intention?

@bsaul
Copy link
Contributor Author

bsaul commented Jan 12, 2026

I agree with @Taneb regarding the RightModule case, but I'd understood that was part of the original intention?

Yep. I'll add these soonish.

@bsaul bsaul changed the title Adds additional properties to LeftModule Adds additional properties to {Left,Right}Module Jan 12, 2026
@bsaul
Copy link
Contributor Author

bsaul commented Jan 12, 2026

Ok -- added RightModule properties.

jamesmckinna
jamesmckinna reviewed Jan 12, 2026
View reviewed changes
jamesmckinna
jamesmckinna reviewed Jan 12, 2026
View reviewed changes
jamesmckinna
jamesmckinna reviewed Jan 12, 2026
View reviewed changes
jamesmckinna
jamesmckinna reviewed Jan 12, 2026
View reviewed changes
@jamesmckinna
Copy link
Collaborator

jamesmckinna commented Jan 12, 2026

Nice! All looks great now. Will merge in the next 24 hours unless we hear objections!

@jamesmckinna jamesmckinna added this pull request to the merge queue Jan 14, 2026
Merged via the queue into agda:master with commit ef2c17c Jan 14, 2026
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jamesmckinna jamesmckinna jamesmckinna approved these changes

@Taneb Taneb Taneb approved these changes

@JacquesCarette JacquesCarette Awaiting requested review from JacquesCarette

Assignees

No one assigned

Labels

addition

Projects

None yet

Milestone

v2.4

Development

Successfully merging this pull request may close these issues.

3 participants

@bsaul @Taneb @jamesmckinna